↳ ITRS

  ↳ ITRStoIDPProof

z

eval(x, y, z) → Cond_eval2(&&(&&(>@z(y, z), >=@z(z, x)), >=@z(z, y)), x, y, z)
Cond_eval5(TRUE, x, y, z) → eval(x, y, z)
Cond_eval2(TRUE, x, y, z) → eval(x, y, z)
eval(x, y, z) → Cond_eval5(&&(&&(>@z(x, z), >=@z(z, x)), >=@z(z, y)), x, y, z)
eval(x, y, z) → Cond_eval4(>@z(x, z), x, y, z)
Cond_eval4(TRUE, x, y, z) → eval(-@z(x, 1@z), y, z)
Cond_eval(TRUE, x, y, z) → eval(-@z(x, 1@z), y, z)
eval(x, y, z) → Cond_eval(&&(>@z(y, z), >@z(x, z)), x, y, z)
Cond_eval1(TRUE, x, y, z) → eval(x, -@z(y, 1@z), z)
eval(x, y, z) → Cond_eval3(&&(&&(>@z(x, z), >=@z(z, x)), >@z(y, z)), x, y, z)
eval(x, y, z) → Cond_eval1(&&(>@z(y, z), >=@z(z, x)), x, y, z)
Cond_eval3(TRUE, x, y, z) → eval(x, -@z(y, 1@z), z)

eval(x0, x1, x2)
Cond_eval5(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
Cond_eval4(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval3(TRUE, x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

z

eval(x, y, z) → Cond_eval2(&&(&&(>@z(y, z), >=@z(z, x)), >=@z(z, y)), x, y, z)
Cond_eval5(TRUE, x, y, z) → eval(x, y, z)
Cond_eval2(TRUE, x, y, z) → eval(x, y, z)
eval(x, y, z) → Cond_eval5(&&(&&(>@z(x, z), >=@z(z, x)), >=@z(z, y)), x, y, z)
eval(x, y, z) → Cond_eval4(>@z(x, z), x, y, z)
Cond_eval4(TRUE, x, y, z) → eval(-@z(x, 1@z), y, z)
Cond_eval(TRUE, x, y, z) → eval(-@z(x, 1@z), y, z)
eval(x, y, z) → Cond_eval(&&(>@z(y, z), >@z(x, z)), x, y, z)
Cond_eval1(TRUE, x, y, z) → eval(x, -@z(y, 1@z), z)
eval(x, y, z) → Cond_eval3(&&(&&(>@z(x, z), >=@z(z, x)), >@z(y, z)), x, y, z)
eval(x, y, z) → Cond_eval1(&&(>@z(y, z), >=@z(z, x)), x, y, z)
Cond_eval3(TRUE, x, y, z) → eval(x, -@z(y, 1@z), z)

(0) -> (1), if ((y[0] →^* y[1])∧(z[0] →^* z[1])∧(-@z(x[0], 1@z) →^* x[1]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(-@z(x[0], 1@z) →^* x[2]))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(-@z(x[0], 1@z) →^* x[3]))

(0) -> (5), if ((y[0] →^* y[5])∧(z[0] →^* z[5])∧(-@z(x[0], 1@z) →^* x[5]))

(0) -> (6), if ((y[0] →^* y[6])∧(z[0] →^* z[6])∧(-@z(x[0], 1@z) →^* x[6]))

(0) -> (10), if ((y[0] →^* y[10])∧(z[0] →^* z[10])∧(-@z(x[0], 1@z) →^* x[10]))

(1) -> (11), if ((z[1] →^* z[11])∧(x[1] →^* x[11])∧(y[1] →^* y[11])∧(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])) →^* TRUE))

(2) -> (0), if ((z[2] →^* z[0])∧(x[2] →^* x[0])∧(y[2] →^* y[0])∧(&&(>@z(y[2], z[2]), >@z(x[2], z[2])) →^* TRUE))

(3) -> (8), if ((z[3] →^* z[8])∧(x[3] →^* x[8])∧(y[3] →^* y[8])∧(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])) →^* TRUE))

(4) -> (1), if ((y[4] →^* y[1])∧(z[4] →^* z[1])∧(-@z(x[4], 1@z) →^* x[1]))

(4) -> (2), if ((y[4] →^* y[2])∧(z[4] →^* z[2])∧(-@z(x[4], 1@z) →^* x[2]))

(4) -> (3), if ((y[4] →^* y[3])∧(z[4] →^* z[3])∧(-@z(x[4], 1@z) →^* x[3]))

(4) -> (5), if ((y[4] →^* y[5])∧(z[4] →^* z[5])∧(-@z(x[4], 1@z) →^* x[5]))

(4) -> (6), if ((y[4] →^* y[6])∧(z[4] →^* z[6])∧(-@z(x[4], 1@z) →^* x[6]))

(4) -> (10), if ((y[4] →^* y[10])∧(z[4] →^* z[10])∧(-@z(x[4], 1@z) →^* x[10]))

(5) -> (9), if ((z[5] →^* z[9])∧(x[5] →^* x[9])∧(y[5] →^* y[9])∧(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])) →^* TRUE))

(6) -> (4), if ((z[6] →^* z[4])∧(x[6] →^* x[4])∧(y[6] →^* y[4])∧(>@z(x[6], z[6]) →^* TRUE))

(7) -> (1), if ((y[7] →^* y[1])∧(z[7] →^* z[1])∧(x[7] →^* x[1]))

(7) -> (2), if ((y[7] →^* y[2])∧(z[7] →^* z[2])∧(x[7] →^* x[2]))

(7) -> (3), if ((y[7] →^* y[3])∧(z[7] →^* z[3])∧(x[7] →^* x[3]))

(7) -> (5), if ((y[7] →^* y[5])∧(z[7] →^* z[5])∧(x[7] →^* x[5]))

(7) -> (6), if ((y[7] →^* y[6])∧(z[7] →^* z[6])∧(x[7] →^* x[6]))

(7) -> (10), if ((y[7] →^* y[10])∧(z[7] →^* z[10])∧(x[7] →^* x[10]))

(8) -> (1), if ((-@z(y[8], 1@z) →^* y[1])∧(z[8] →^* z[1])∧(x[8] →^* x[1]))

(8) -> (2), if ((-@z(y[8], 1@z) →^* y[2])∧(z[8] →^* z[2])∧(x[8] →^* x[2]))

(8) -> (3), if ((-@z(y[8], 1@z) →^* y[3])∧(z[8] →^* z[3])∧(x[8] →^* x[3]))

(8) -> (5), if ((-@z(y[8], 1@z) →^* y[5])∧(z[8] →^* z[5])∧(x[8] →^* x[5]))

(8) -> (6), if ((-@z(y[8], 1@z) →^* y[6])∧(z[8] →^* z[6])∧(x[8] →^* x[6]))

(8) -> (10), if ((-@z(y[8], 1@z) →^* y[10])∧(z[8] →^* z[10])∧(x[8] →^* x[10]))

(9) -> (1), if ((y[9] →^* y[1])∧(z[9] →^* z[1])∧(x[9] →^* x[1]))

(9) -> (2), if ((y[9] →^* y[2])∧(z[9] →^* z[2])∧(x[9] →^* x[2]))

(9) -> (3), if ((y[9] →^* y[3])∧(z[9] →^* z[3])∧(x[9] →^* x[3]))

(9) -> (5), if ((y[9] →^* y[5])∧(z[9] →^* z[5])∧(x[9] →^* x[5]))

(9) -> (6), if ((y[9] →^* y[6])∧(z[9] →^* z[6])∧(x[9] →^* x[6]))

(9) -> (10), if ((y[9] →^* y[10])∧(z[9] →^* z[10])∧(x[9] →^* x[10]))

(10) -> (7), if ((z[10] →^* z[7])∧(x[10] →^* x[7])∧(y[10] →^* y[7])∧(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])) →^* TRUE))

(11) -> (1), if ((-@z(y[11], 1@z) →^* y[1])∧(z[11] →^* z[1])∧(x[11] →^* x[1]))

(11) -> (2), if ((-@z(y[11], 1@z) →^* y[2])∧(z[11] →^* z[2])∧(x[11] →^* x[2]))

(11) -> (3), if ((-@z(y[11], 1@z) →^* y[3])∧(z[11] →^* z[3])∧(x[11] →^* x[3]))

(11) -> (5), if ((-@z(y[11], 1@z) →^* y[5])∧(z[11] →^* z[5])∧(x[11] →^* x[5]))

(11) -> (6), if ((-@z(y[11], 1@z) →^* y[6])∧(z[11] →^* z[6])∧(x[11] →^* x[6]))

(11) -> (10), if ((-@z(y[11], 1@z) →^* y[10])∧(z[11] →^* z[10])∧(x[11] →^* x[10]))

eval(x0, x1, x2)
Cond_eval5(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
Cond_eval4(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval3(TRUE, x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

z

(0) -> (1), if ((y[0] →^* y[1])∧(z[0] →^* z[1])∧(-@z(x[0], 1@z) →^* x[1]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(-@z(x[0], 1@z) →^* x[2]))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(-@z(x[0], 1@z) →^* x[3]))

(0) -> (5), if ((y[0] →^* y[5])∧(z[0] →^* z[5])∧(-@z(x[0], 1@z) →^* x[5]))

(0) -> (6), if ((y[0] →^* y[6])∧(z[0] →^* z[6])∧(-@z(x[0], 1@z) →^* x[6]))

(0) -> (10), if ((y[0] →^* y[10])∧(z[0] →^* z[10])∧(-@z(x[0], 1@z) →^* x[10]))

(1) -> (11), if ((z[1] →^* z[11])∧(x[1] →^* x[11])∧(y[1] →^* y[11])∧(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])) →^* TRUE))

(2) -> (0), if ((z[2] →^* z[0])∧(x[2] →^* x[0])∧(y[2] →^* y[0])∧(&&(>@z(y[2], z[2]), >@z(x[2], z[2])) →^* TRUE))

(3) -> (8), if ((z[3] →^* z[8])∧(x[3] →^* x[8])∧(y[3] →^* y[8])∧(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])) →^* TRUE))

(4) -> (1), if ((y[4] →^* y[1])∧(z[4] →^* z[1])∧(-@z(x[4], 1@z) →^* x[1]))

(4) -> (2), if ((y[4] →^* y[2])∧(z[4] →^* z[2])∧(-@z(x[4], 1@z) →^* x[2]))

(4) -> (3), if ((y[4] →^* y[3])∧(z[4] →^* z[3])∧(-@z(x[4], 1@z) →^* x[3]))

(4) -> (5), if ((y[4] →^* y[5])∧(z[4] →^* z[5])∧(-@z(x[4], 1@z) →^* x[5]))

(4) -> (6), if ((y[4] →^* y[6])∧(z[4] →^* z[6])∧(-@z(x[4], 1@z) →^* x[6]))

(4) -> (10), if ((y[4] →^* y[10])∧(z[4] →^* z[10])∧(-@z(x[4], 1@z) →^* x[10]))

(5) -> (9), if ((z[5] →^* z[9])∧(x[5] →^* x[9])∧(y[5] →^* y[9])∧(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])) →^* TRUE))

(6) -> (4), if ((z[6] →^* z[4])∧(x[6] →^* x[4])∧(y[6] →^* y[4])∧(>@z(x[6], z[6]) →^* TRUE))

(7) -> (1), if ((y[7] →^* y[1])∧(z[7] →^* z[1])∧(x[7] →^* x[1]))

(7) -> (2), if ((y[7] →^* y[2])∧(z[7] →^* z[2])∧(x[7] →^* x[2]))

(7) -> (3), if ((y[7] →^* y[3])∧(z[7] →^* z[3])∧(x[7] →^* x[3]))

(7) -> (5), if ((y[7] →^* y[5])∧(z[7] →^* z[5])∧(x[7] →^* x[5]))

(7) -> (6), if ((y[7] →^* y[6])∧(z[7] →^* z[6])∧(x[7] →^* x[6]))

(7) -> (10), if ((y[7] →^* y[10])∧(z[7] →^* z[10])∧(x[7] →^* x[10]))

(8) -> (1), if ((-@z(y[8], 1@z) →^* y[1])∧(z[8] →^* z[1])∧(x[8] →^* x[1]))

(8) -> (2), if ((-@z(y[8], 1@z) →^* y[2])∧(z[8] →^* z[2])∧(x[8] →^* x[2]))

(8) -> (3), if ((-@z(y[8], 1@z) →^* y[3])∧(z[8] →^* z[3])∧(x[8] →^* x[3]))

(8) -> (5), if ((-@z(y[8], 1@z) →^* y[5])∧(z[8] →^* z[5])∧(x[8] →^* x[5]))

(8) -> (6), if ((-@z(y[8], 1@z) →^* y[6])∧(z[8] →^* z[6])∧(x[8] →^* x[6]))

(8) -> (10), if ((-@z(y[8], 1@z) →^* y[10])∧(z[8] →^* z[10])∧(x[8] →^* x[10]))

(9) -> (1), if ((y[9] →^* y[1])∧(z[9] →^* z[1])∧(x[9] →^* x[1]))

(9) -> (2), if ((y[9] →^* y[2])∧(z[9] →^* z[2])∧(x[9] →^* x[2]))

(9) -> (3), if ((y[9] →^* y[3])∧(z[9] →^* z[3])∧(x[9] →^* x[3]))

(9) -> (5), if ((y[9] →^* y[5])∧(z[9] →^* z[5])∧(x[9] →^* x[5]))

(9) -> (6), if ((y[9] →^* y[6])∧(z[9] →^* z[6])∧(x[9] →^* x[6]))

(9) -> (10), if ((y[9] →^* y[10])∧(z[9] →^* z[10])∧(x[9] →^* x[10]))

(10) -> (7), if ((z[10] →^* z[7])∧(x[10] →^* x[7])∧(y[10] →^* y[7])∧(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])) →^* TRUE))

(11) -> (1), if ((-@z(y[11], 1@z) →^* y[1])∧(z[11] →^* z[1])∧(x[11] →^* x[1]))

(11) -> (2), if ((-@z(y[11], 1@z) →^* y[2])∧(z[11] →^* z[2])∧(x[11] →^* x[2]))

(11) -> (3), if ((-@z(y[11], 1@z) →^* y[3])∧(z[11] →^* z[3])∧(x[11] →^* x[3]))

(11) -> (5), if ((-@z(y[11], 1@z) →^* y[5])∧(z[11] →^* z[5])∧(x[11] →^* x[5]))

(11) -> (6), if ((-@z(y[11], 1@z) →^* y[6])∧(z[11] →^* z[6])∧(x[11] →^* x[6]))

(11) -> (10), if ((-@z(y[11], 1@z) →^* y[10])∧(z[11] →^* z[10])∧(x[11] →^* x[10]))

eval(x0, x1, x2)
Cond_eval5(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
Cond_eval4(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval3(TRUE, x0, x1, x2)

• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2]), COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(-@z(x[0], 1@z), y[0], z[0]) which results in the following constraint:
  

  (1)    (z[2]=z[0]∧x[2]=x[0]∧&&(>@z(y[2], z[2]), >@z(x[2], z[2]))=TRUE∧y[2]=y[0] ⇒ COND_EVAL(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL(TRUE, x[0], y[0], z[0])≥EVAL(-@z(x[0], 1@z), y[0], z[0])∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (1) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>@z(y[2], z[2])=TRUE∧>@z(x[2], z[2])=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(-@z(x[2], 1@z), y[2], z[2])∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (y[2] + -1 + (-1)z[2] ≥ 0∧-1 + x[2] + (-1)z[2] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (y[2] + -1 + (-1)z[2] ≥ 0∧-1 + x[2] + (-1)z[2] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (-1 + x[2] + (-1)z[2] ≥ 0∧y[2] + -1 + (-1)z[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (x[2] ≥ 0∧y[2] + -1 + (-1)z[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (x[2] ≥ 0∧z[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (8)    (x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)

  
  

  (9)    (x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)

  
  
  

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1]) which results in the following constraint:
  

  (10)    (EVAL(x[1], y[1], z[1])≥NonInfC∧EVAL(x[1], y[1], z[1])≥COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (11)    ((U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (12)    ((U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (13)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (14)    (0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2]) which results in the following constraint:
  

  (15)    (EVAL(x[2], y[2], z[2])≥NonInfC∧EVAL(x[2], y[2], z[2])≥COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥))

  
  
  We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (16)    ((U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (17)    ((U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (18)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥))

  
  
  We simplified constraint (18) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (19)    (0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3]) which results in the following constraint:
  

  (20)    (EVAL(x[3], y[3], z[3])≥NonInfC∧EVAL(x[3], y[3], z[3])≥COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (21)    ((U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (22)    ((U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (23)    (1 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (24)    (0 = 0∧0 = 0∧1 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥))

  
  
  

• We consider the chain EVAL(x[6], y[6], z[6]) → COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6]), COND_EVAL4(TRUE, x[4], y[4], z[4]) → EVAL(-@z(x[4], 1@z), y[4], z[4]) which results in the following constraint:
  

  (25)    (y[6]=y[4]∧x[6]=x[4]∧>@z(x[6], z[6])=TRUE∧z[6]=z[4] ⇒ COND_EVAL4(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL4(TRUE, x[4], y[4], z[4])≥EVAL(-@z(x[4], 1@z), y[4], z[4])∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (25) using rule (III) which results in the following new constraint:
  

  (26)    (>@z(x[6], z[6])=TRUE ⇒ COND_EVAL4(TRUE, x[6], y[6], z[6])≥NonInfC∧COND_EVAL4(TRUE, x[6], y[6], z[6])≥EVAL(-@z(x[6], 1@z), y[6], z[6])∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (27)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (28)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (29)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (30)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (31)    (x[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (31) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (32)    (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0)

  
  

  (33)    (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0)

  
  
  

• We consider the chain EVAL(x[5], y[5], z[5]) → COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5]) which results in the following constraint:
  

  (34)    (EVAL(x[5], y[5], z[5])≥NonInfC∧EVAL(x[5], y[5], z[5])≥COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])∧(U^Increasing(COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])), ≥))

  
  
  We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (35)    ((U^Increasing(COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (36)    ((U^Increasing(COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (37)    ((U^Increasing(COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])), ≥)∧1 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (38)    (1 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])), ≥)∧0 = 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[6], y[6], z[6]) → COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6]) which results in the following constraint:
  

  (39)    (EVAL(x[6], y[6], z[6])≥NonInfC∧EVAL(x[6], y[6], z[6])≥COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥))

  
  
  We simplified constraint (39) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (40)    ((U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (40) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (41)    ((U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (41) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (42)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥))

  
  
  We simplified constraint (42) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (43)    (0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥)∧0 = 0)

  
  
  

• We consider the chain EVAL(x[10], y[10], z[10]) → COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10]), COND_EVAL5(TRUE, x[7], y[7], z[7]) → EVAL(x[7], y[7], z[7]) which results in the following constraint:
  

  (44)    (z[10]=z[7]∧y[10]=y[7]∧x[10]=x[7]∧&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10]))=TRUE ⇒ COND_EVAL5(TRUE, x[7], y[7], z[7])≥NonInfC∧COND_EVAL5(TRUE, x[7], y[7], z[7])≥EVAL(x[7], y[7], z[7])∧(U^Increasing(EVAL(x[7], y[7], z[7])), ≥))

  
  
  We simplified constraint (44) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (45)    (>=@z(z[10], y[10])=TRUE∧>@z(x[10], z[10])=TRUE∧>=@z(z[10], x[10])=TRUE ⇒ COND_EVAL5(TRUE, x[10], y[10], z[10])≥NonInfC∧COND_EVAL5(TRUE, x[10], y[10], z[10])≥EVAL(x[10], y[10], z[10])∧(U^Increasing(EVAL(x[7], y[7], z[7])), ≥))

  
  
  We simplified constraint (45) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (46)    (z[10] + (-1)y[10] ≥ 0∧-1 + x[10] + (-1)z[10] ≥ 0∧z[10] + (-1)x[10] ≥ 0 ⇒ (U^Increasing(EVAL(x[7], y[7], z[7])), ≥)∧0 ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (46) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (47)    (z[10] + (-1)y[10] ≥ 0∧-1 + x[10] + (-1)z[10] ≥ 0∧z[10] + (-1)x[10] ≥ 0 ⇒ (U^Increasing(EVAL(x[7], y[7], z[7])), ≥)∧0 ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (47) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (48)    (z[10] + (-1)y[10] ≥ 0∧z[10] + (-1)x[10] ≥ 0∧-1 + x[10] + (-1)z[10] ≥ 0 ⇒ (U^Increasing(EVAL(x[7], y[7], z[7])), ≥)∧-1 ≥ 0∧0 ≥ 0)

  
  
  We solved constraint (48) using rule (IDP_SMT_SPLIT).

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3]), COND_EVAL3(TRUE, x[8], y[8], z[8]) → EVAL(x[8], -@z(y[8], 1@z), z[8]) which results in the following constraint:
  

  (49)    (&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3]))=TRUE∧z[3]=z[8]∧x[3]=x[8]∧y[3]=y[8] ⇒ COND_EVAL3(TRUE, x[8], y[8], z[8])≥NonInfC∧COND_EVAL3(TRUE, x[8], y[8], z[8])≥EVAL(x[8], -@z(y[8], 1@z), z[8])∧(U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥))

  
  
  We simplified constraint (49) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (50)    (>@z(y[3], z[3])=TRUE∧>@z(x[3], z[3])=TRUE∧>=@z(z[3], x[3])=TRUE ⇒ COND_EVAL3(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL3(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥))

  
  
  We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (51)    (-1 + y[3] + (-1)z[3] ≥ 0∧-1 + x[3] + (-1)z[3] ≥ 0∧z[3] + (-1)x[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥)∧0 ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (52)    (-1 + y[3] + (-1)z[3] ≥ 0∧-1 + x[3] + (-1)z[3] ≥ 0∧z[3] + (-1)x[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥)∧0 ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (53)    (z[3] + (-1)x[3] ≥ 0∧-1 + x[3] + (-1)z[3] ≥ 0∧-1 + y[3] + (-1)z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥)∧-1 ≥ 0∧0 ≥ 0)

  
  
  We solved constraint (53) using rule (IDP_SMT_SPLIT).

• We consider the chain EVAL(x[5], y[5], z[5]) → COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5]), COND_EVAL2(TRUE, x[9], y[9], z[9]) → EVAL(x[9], y[9], z[9]) which results in the following constraint:
  

  (54)    (x[5]=x[9]∧&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5]))=TRUE∧y[5]=y[9]∧z[5]=z[9] ⇒ COND_EVAL2(TRUE, x[9], y[9], z[9])≥NonInfC∧COND_EVAL2(TRUE, x[9], y[9], z[9])≥EVAL(x[9], y[9], z[9])∧(U^Increasing(EVAL(x[9], y[9], z[9])), ≥))

  
  
  We simplified constraint (54) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (55)    (>=@z(z[5], y[5])=TRUE∧>@z(y[5], z[5])=TRUE∧>=@z(z[5], x[5])=TRUE ⇒ COND_EVAL2(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL2(TRUE, x[5], y[5], z[5])≥EVAL(x[5], y[5], z[5])∧(U^Increasing(EVAL(x[9], y[9], z[9])), ≥))

  
  
  We simplified constraint (55) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (56)    (z[5] + (-1)y[5] ≥ 0∧-1 + y[5] + (-1)z[5] ≥ 0∧z[5] + (-1)x[5] ≥ 0 ⇒ (U^Increasing(EVAL(x[9], y[9], z[9])), ≥)∧-2 + (-1)Bound + (-1)z[5] ≥ 0∧-2 ≥ 0)

  
  
  We simplified constraint (56) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (57)    (z[5] + (-1)y[5] ≥ 0∧-1 + y[5] + (-1)z[5] ≥ 0∧z[5] + (-1)x[5] ≥ 0 ⇒ (U^Increasing(EVAL(x[9], y[9], z[9])), ≥)∧-2 + (-1)Bound + (-1)z[5] ≥ 0∧-2 ≥ 0)

  
  
  We simplified constraint (57) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (58)    (-1 + y[5] + (-1)z[5] ≥ 0∧z[5] + (-1)x[5] ≥ 0∧z[5] + (-1)y[5] ≥ 0 ⇒ -2 + (-1)Bound + (-1)z[5] ≥ 0∧(U^Increasing(EVAL(x[9], y[9], z[9])), ≥)∧-2 ≥ 0)

  
  
  We solved constraint (58) using rule (IDP_SMT_SPLIT).

• We consider the chain EVAL(x[10], y[10], z[10]) → COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10]) which results in the following constraint:
  

  (59)    (EVAL(x[10], y[10], z[10])≥NonInfC∧EVAL(x[10], y[10], z[10])≥COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥))

  
  
  We simplified constraint (59) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (60)    ((U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (60) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (61)    ((U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (61) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (62)    (0 ≥ 0∧1 ≥ 0∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥))

  
  
  We simplified constraint (62) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (63)    (0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧1 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[11], y[11], z[11]) → EVAL(x[11], -@z(y[11], 1@z), z[11]) which results in the following constraint:
  

  (64)    (&&(>@z(y[1], z[1]), >=@z(z[1], x[1]))=TRUE∧y[1]=y[11]∧x[1]=x[11]∧z[1]=z[11] ⇒ COND_EVAL1(TRUE, x[11], y[11], z[11])≥NonInfC∧COND_EVAL1(TRUE, x[11], y[11], z[11])≥EVAL(x[11], -@z(y[11], 1@z), z[11])∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (64) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (65)    (>@z(y[1], z[1])=TRUE∧>=@z(z[1], x[1])=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(x[1], -@z(y[1], 1@z), z[1])∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (65) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (66)    (-1 + y[1] + (-1)z[1] ≥ 0∧z[1] + (-1)x[1] ≥ 0 ⇒ (U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (66) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (67)    (-1 + y[1] + (-1)z[1] ≥ 0∧z[1] + (-1)x[1] ≥ 0 ⇒ (U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (67) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (68)    (z[1] + (-1)x[1] ≥ 0∧-1 + y[1] + (-1)z[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (68) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (69)    (x[1] ≥ 0∧-1 + y[1] + (-1)z[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (69) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (70)    (x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (70) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (71)    (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  

  (72)    (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  

• COND_EVAL(TRUE, x, y, z) → EVAL(-@z(x, 1@z), y, z)
  
  • (x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)
    
  • (x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL1(&&(>@z(y, z), >=@z(z, x)), x, y, z)
  
  • (0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 = 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL(&&(>@z(y, z), >@z(x, z)), x, y, z)
  
  • (0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 = 0∧0 = 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL3(&&(&&(>@z(x, z), >=@z(z, x)), >@z(y, z)), x, y, z)
  
  • (0 = 0∧0 = 0∧1 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥))
    
  
  
• COND_EVAL4(TRUE, x, y, z) → EVAL(-@z(x, 1@z), y, z)
  
  • (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0)
    
  • (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL2(&&(&&(>@z(y, z), >=@z(z, x)), >=@z(z, y)), x, y, z)
  
  • (1 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])), ≥)∧0 = 0∧0 = 0∧0 = 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL4(>@z(x, z), x, y, z)
  
  • (0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥)∧0 = 0)
    
  
  
• COND_EVAL5(TRUE, x, y, z) → EVAL(x, y, z)
  
  
• COND_EVAL3(TRUE, x, y, z) → EVAL(x, -@z(y, 1@z), z)
  
  
• COND_EVAL2(TRUE, x, y, z) → EVAL(x, y, z)
  
  
• EVAL(x, y, z) → COND_EVAL5(&&(&&(>@z(x, z), >=@z(z, x)), >=@z(z, y)), x, y, z)
  
  • (0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧1 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 = 0∧0 = 0)
    
  
  
• COND_EVAL1(TRUE, x, y, z) → EVAL(x, -@z(y, 1@z), z)
  
  • (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))
    
  • (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))
    
  
  

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂   
POL(COND_EVAL2(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₁   
POL(COND_EVAL3(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₁   
POL(TRUE) = -1   
POL(&&(x₁, x₂)) = -1   
POL(EVAL(x₁, x₂, x₃)) = -1 + (-1)x₃   
POL(FALSE) = -1   
POL(>@z(x₁, x₂)) = -1   
POL(COND_EVAL5(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₁   
POL(>=@z(x₁, x₂)) = -1   
POL(COND_EVAL1(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄   
POL(COND_EVAL(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄   
POL(COND_EVAL4(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄   
POL(1@z) = 1   
POL(undefined) = -1   

COND_EVAL2(TRUE, x[9], y[9], z[9]) → EVAL(x[9], y[9], z[9])

COND_EVAL2(TRUE, x[9], y[9], z[9]) → EVAL(x[9], y[9], z[9])

COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(-@z(x[0], 1@z), y[0], z[0])
EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])
EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])
EVAL(x[3], y[3], z[3]) → COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])
COND_EVAL4(TRUE, x[4], y[4], z[4]) → EVAL(-@z(x[4], 1@z), y[4], z[4])
EVAL(x[5], y[5], z[5]) → COND_EVAL2(&&(&&(>@z(y[5], z[5]), >=@z(z[5], x[5])), >=@z(z[5], y[5])), x[5], y[5], z[5])
EVAL(x[6], y[6], z[6]) → COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])
COND_EVAL5(TRUE, x[7], y[7], z[7]) → EVAL(x[7], y[7], z[7])
COND_EVAL3(TRUE, x[8], y[8], z[8]) → EVAL(x[8], -@z(y[8], 1@z), z[8])
EVAL(x[10], y[10], z[10]) → COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])
COND_EVAL1(TRUE, x[11], y[11], z[11]) → EVAL(x[11], -@z(y[11], 1@z), z[11])

&&(FALSE, FALSE)¹ → FALSE¹
-@z¹ ↔
&&(TRUE, TRUE)¹ → TRUE¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

z

(0) -> (6), if ((y[0] →^* y[6])∧(z[0] →^* z[6])∧(-@z(x[0], 1@z) →^* x[6]))

(6) -> (4), if ((z[6] →^* z[4])∧(x[6] →^* x[4])∧(y[6] →^* y[4])∧(>@z(x[6], z[6]) →^* TRUE))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(-@z(x[0], 1@z) →^* x[3]))

(7) -> (3), if ((y[7] →^* y[3])∧(z[7] →^* z[3])∧(x[7] →^* x[3]))

(8) -> (1), if ((-@z(y[8], 1@z) →^* y[1])∧(z[8] →^* z[1])∧(x[8] →^* x[1]))

(2) -> (0), if ((z[2] →^* z[0])∧(x[2] →^* x[0])∧(y[2] →^* y[0])∧(&&(>@z(y[2], z[2]), >@z(x[2], z[2])) →^* TRUE))

(3) -> (8), if ((z[3] →^* z[8])∧(x[3] →^* x[8])∧(y[3] →^* y[8])∧(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])) →^* TRUE))

(11) -> (10), if ((-@z(y[11], 1@z) →^* y[10])∧(z[11] →^* z[10])∧(x[11] →^* x[10]))

(4) -> (10), if ((y[4] →^* y[10])∧(z[4] →^* z[10])∧(-@z(x[4], 1@z) →^* x[10]))

(11) -> (6), if ((-@z(y[11], 1@z) →^* y[6])∧(z[11] →^* z[6])∧(x[11] →^* x[6]))

(8) -> (5), if ((-@z(y[8], 1@z) →^* y[5])∧(z[8] →^* z[5])∧(x[8] →^* x[5]))

(7) -> (5), if ((y[7] →^* y[5])∧(z[7] →^* z[5])∧(x[7] →^* x[5]))

(4) -> (3), if ((y[4] →^* y[3])∧(z[4] →^* z[3])∧(-@z(x[4], 1@z) →^* x[3]))

(7) -> (6), if ((y[7] →^* y[6])∧(z[7] →^* z[6])∧(x[7] →^* x[6]))

(1) -> (11), if ((z[1] →^* z[11])∧(x[1] →^* x[11])∧(y[1] →^* y[11])∧(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])) →^* TRUE))

(0) -> (1), if ((y[0] →^* y[1])∧(z[0] →^* z[1])∧(-@z(x[0], 1@z) →^* x[1]))

(10) -> (7), if ((z[10] →^* z[7])∧(x[10] →^* x[7])∧(y[10] →^* y[7])∧(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])) →^* TRUE))

(11) -> (2), if ((-@z(y[11], 1@z) →^* y[2])∧(z[11] →^* z[2])∧(x[11] →^* x[2]))

(0) -> (5), if ((y[0] →^* y[5])∧(z[0] →^* z[5])∧(-@z(x[0], 1@z) →^* x[5]))

(4) -> (6), if ((y[4] →^* y[6])∧(z[4] →^* z[6])∧(-@z(x[4], 1@z) →^* x[6]))

(8) -> (6), if ((-@z(y[8], 1@z) →^* y[6])∧(z[8] →^* z[6])∧(x[8] →^* x[6]))

(8) -> (10), if ((-@z(y[8], 1@z) →^* y[10])∧(z[8] →^* z[10])∧(x[8] →^* x[10]))

(11) -> (3), if ((-@z(y[11], 1@z) →^* y[3])∧(z[11] →^* z[3])∧(x[11] →^* x[3]))

(7) -> (2), if ((y[7] →^* y[2])∧(z[7] →^* z[2])∧(x[7] →^* x[2]))

(7) -> (10), if ((y[7] →^* y[10])∧(z[7] →^* z[10])∧(x[7] →^* x[10]))

(8) -> (2), if ((-@z(y[8], 1@z) →^* y[2])∧(z[8] →^* z[2])∧(x[8] →^* x[2]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(-@z(x[0], 1@z) →^* x[2]))

(0) -> (10), if ((y[0] →^* y[10])∧(z[0] →^* z[10])∧(-@z(x[0], 1@z) →^* x[10]))

(4) -> (1), if ((y[4] →^* y[1])∧(z[4] →^* z[1])∧(-@z(x[4], 1@z) →^* x[1]))

(8) -> (3), if ((-@z(y[8], 1@z) →^* y[3])∧(z[8] →^* z[3])∧(x[8] →^* x[3]))

(4) -> (2), if ((y[4] →^* y[2])∧(z[4] →^* z[2])∧(-@z(x[4], 1@z) →^* x[2]))

(11) -> (5), if ((-@z(y[11], 1@z) →^* y[5])∧(z[11] →^* z[5])∧(x[11] →^* x[5]))

(7) -> (1), if ((y[7] →^* y[1])∧(z[7] →^* z[1])∧(x[7] →^* x[1]))

(11) -> (1), if ((-@z(y[11], 1@z) →^* y[1])∧(z[11] →^* z[1])∧(x[11] →^* x[1]))

(4) -> (5), if ((y[4] →^* y[5])∧(z[4] →^* z[5])∧(-@z(x[4], 1@z) →^* x[5]))

eval(x0, x1, x2)
Cond_eval5(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
Cond_eval4(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval3(TRUE, x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

z

(0) -> (6), if ((y[0] →^* y[6])∧(z[0] →^* z[6])∧(-@z(x[0], 1@z) →^* x[6]))

(6) -> (4), if ((z[6] →^* z[4])∧(x[6] →^* x[4])∧(y[6] →^* y[4])∧(>@z(x[6], z[6]) →^* TRUE))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(-@z(x[0], 1@z) →^* x[3]))

(7) -> (3), if ((y[7] →^* y[3])∧(z[7] →^* z[3])∧(x[7] →^* x[3]))

(8) -> (1), if ((-@z(y[8], 1@z) →^* y[1])∧(z[8] →^* z[1])∧(x[8] →^* x[1]))

(3) -> (8), if ((z[3] →^* z[8])∧(x[3] →^* x[8])∧(y[3] →^* y[8])∧(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])) →^* TRUE))

(2) -> (0), if ((z[2] →^* z[0])∧(x[2] →^* x[0])∧(y[2] →^* y[0])∧(&&(>@z(y[2], z[2]), >@z(x[2], z[2])) →^* TRUE))

(11) -> (10), if ((-@z(y[11], 1@z) →^* y[10])∧(z[11] →^* z[10])∧(x[11] →^* x[10]))

(4) -> (10), if ((y[4] →^* y[10])∧(z[4] →^* z[10])∧(-@z(x[4], 1@z) →^* x[10]))

(11) -> (6), if ((-@z(y[11], 1@z) →^* y[6])∧(z[11] →^* z[6])∧(x[11] →^* x[6]))

(4) -> (3), if ((y[4] →^* y[3])∧(z[4] →^* z[3])∧(-@z(x[4], 1@z) →^* x[3]))

(7) -> (6), if ((y[7] →^* y[6])∧(z[7] →^* z[6])∧(x[7] →^* x[6]))

(1) -> (11), if ((z[1] →^* z[11])∧(x[1] →^* x[11])∧(y[1] →^* y[11])∧(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])) →^* TRUE))

(0) -> (1), if ((y[0] →^* y[1])∧(z[0] →^* z[1])∧(-@z(x[0], 1@z) →^* x[1]))

(10) -> (7), if ((z[10] →^* z[7])∧(x[10] →^* x[7])∧(y[10] →^* y[7])∧(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])) →^* TRUE))

(11) -> (2), if ((-@z(y[11], 1@z) →^* y[2])∧(z[11] →^* z[2])∧(x[11] →^* x[2]))

(4) -> (6), if ((y[4] →^* y[6])∧(z[4] →^* z[6])∧(-@z(x[4], 1@z) →^* x[6]))

(8) -> (10), if ((-@z(y[8], 1@z) →^* y[10])∧(z[8] →^* z[10])∧(x[8] →^* x[10]))

(8) -> (6), if ((-@z(y[8], 1@z) →^* y[6])∧(z[8] →^* z[6])∧(x[8] →^* x[6]))

(11) -> (3), if ((-@z(y[11], 1@z) →^* y[3])∧(z[11] →^* z[3])∧(x[11] →^* x[3]))

(7) -> (10), if ((y[7] →^* y[10])∧(z[7] →^* z[10])∧(x[7] →^* x[10]))

(7) -> (2), if ((y[7] →^* y[2])∧(z[7] →^* z[2])∧(x[7] →^* x[2]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(-@z(x[0], 1@z) →^* x[2]))

(8) -> (2), if ((-@z(y[8], 1@z) →^* y[2])∧(z[8] →^* z[2])∧(x[8] →^* x[2]))

(0) -> (10), if ((y[0] →^* y[10])∧(z[0] →^* z[10])∧(-@z(x[0], 1@z) →^* x[10]))

(4) -> (1), if ((y[4] →^* y[1])∧(z[4] →^* z[1])∧(-@z(x[4], 1@z) →^* x[1]))

(8) -> (3), if ((-@z(y[8], 1@z) →^* y[3])∧(z[8] →^* z[3])∧(x[8] →^* x[3]))

(4) -> (2), if ((y[4] →^* y[2])∧(z[4] →^* z[2])∧(-@z(x[4], 1@z) →^* x[2]))

(7) -> (1), if ((y[7] →^* y[1])∧(z[7] →^* z[1])∧(x[7] →^* x[1]))

(11) -> (1), if ((-@z(y[11], 1@z) →^* y[1])∧(z[11] →^* z[1])∧(x[11] →^* x[1]))

eval(x0, x1, x2)
Cond_eval5(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
Cond_eval4(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval3(TRUE, x0, x1, x2)

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[11], y[11], z[11]) → EVAL(x[11], -@z(y[11], 1@z), z[11]) which results in the following constraint:
  

  (1)    (&&(>@z(y[1], z[1]), >=@z(z[1], x[1]))=TRUE∧y[1]=y[11]∧x[1]=x[11]∧z[1]=z[11] ⇒ COND_EVAL1(TRUE, x[11], y[11], z[11])≥NonInfC∧COND_EVAL1(TRUE, x[11], y[11], z[11])≥EVAL(x[11], -@z(y[11], 1@z), z[11])∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (1) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>@z(y[1], z[1])=TRUE∧>=@z(z[1], x[1])=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(x[1], -@z(y[1], 1@z), z[1])∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (-1 + y[1] + (-1)z[1] ≥ 0∧z[1] + (-1)x[1] ≥ 0 ⇒ (U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (-1 + y[1] + (-1)z[1] ≥ 0∧z[1] + (-1)x[1] ≥ 0 ⇒ (U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (z[1] + (-1)x[1] ≥ 0∧-1 + y[1] + (-1)z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (x[1] ≥ 0∧-1 + y[1] + (-1)z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (x[1] ≥ 0∧y[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧(-1)Bound + y[1] ≥ 0)

  
  
  We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (8)    (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧(-1)Bound + y[1] ≥ 0)

  
  

  (9)    (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧(-1)Bound + y[1] ≥ 0)

  
  
  

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1]) which results in the following constraint:
  

  (10)    (EVAL(x[1], y[1], z[1])≥NonInfC∧EVAL(x[1], y[1], z[1])≥COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (11)    ((U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (12)    ((U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (13)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (14)    (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 = 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2]), COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(-@z(x[0], 1@z), y[0], z[0]) which results in the following constraint:
  

  (15)    (z[2]=z[0]∧x[2]=x[0]∧&&(>@z(y[2], z[2]), >@z(x[2], z[2]))=TRUE∧y[2]=y[0] ⇒ COND_EVAL(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL(TRUE, x[0], y[0], z[0])≥EVAL(-@z(x[0], 1@z), y[0], z[0])∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (15) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (16)    (>@z(y[2], z[2])=TRUE∧>@z(x[2], z[2])=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(-@z(x[2], 1@z), y[2], z[2])∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (17)    (y[2] + -1 + (-1)z[2] ≥ 0∧-1 + x[2] + (-1)z[2] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (18)    (y[2] + -1 + (-1)z[2] ≥ 0∧-1 + x[2] + (-1)z[2] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (19)    (y[2] + -1 + (-1)z[2] ≥ 0∧-1 + x[2] + (-1)z[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (20)    (y[2] + -1 + (-1)z[2] ≥ 0∧x[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (21)    (z[2] ≥ 0∧x[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (22)    (z[2] ≥ 0∧x[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  

  (23)    (z[2] ≥ 0∧x[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))

  
  
  

• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2]) which results in the following constraint:
  

  (24)    (EVAL(x[2], y[2], z[2])≥NonInfC∧EVAL(x[2], y[2], z[2])≥COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥))

  
  
  We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (25)    ((U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (26)    ((U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (27)    (0 ≥ 0∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (28)    (0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥))

  
  
  

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3]), COND_EVAL3(TRUE, x[8], y[8], z[8]) → EVAL(x[8], -@z(y[8], 1@z), z[8]) which results in the following constraint:
  

  (29)    (&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3]))=TRUE∧z[3]=z[8]∧x[3]=x[8]∧y[3]=y[8] ⇒ COND_EVAL3(TRUE, x[8], y[8], z[8])≥NonInfC∧COND_EVAL3(TRUE, x[8], y[8], z[8])≥EVAL(x[8], -@z(y[8], 1@z), z[8])∧(U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥))

  
  
  We simplified constraint (29) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (30)    (>@z(y[3], z[3])=TRUE∧>@z(x[3], z[3])=TRUE∧>=@z(z[3], x[3])=TRUE ⇒ COND_EVAL3(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL3(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥))

  
  
  We simplified constraint (30) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (31)    (-1 + y[3] + (-1)z[3] ≥ 0∧-1 + x[3] + (-1)z[3] ≥ 0∧z[3] + (-1)x[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥)∧-1 + (-1)Bound + (-1)z[3] + y[3] ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (31) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (32)    (-1 + y[3] + (-1)z[3] ≥ 0∧-1 + x[3] + (-1)z[3] ≥ 0∧z[3] + (-1)x[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥)∧-1 + (-1)Bound + (-1)z[3] + y[3] ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (32) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (33)    (-1 + y[3] + (-1)z[3] ≥ 0∧-1 + x[3] + (-1)z[3] ≥ 0∧z[3] + (-1)x[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[8], -@z(y[8], 1@z), z[8])), ≥)∧1 ≥ 0∧-1 + (-1)Bound + (-1)z[3] + y[3] ≥ 0)

  
  
  We solved constraint (33) using rule (IDP_SMT_SPLIT).

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3]) which results in the following constraint:
  

  (34)    (EVAL(x[3], y[3], z[3])≥NonInfC∧EVAL(x[3], y[3], z[3])≥COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (35)    ((U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (36)    ((U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (37)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (38)    (0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥)∧0 ≥ 0)

  
  
  

• We consider the chain EVAL(x[10], y[10], z[10]) → COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10]), COND_EVAL5(TRUE, x[7], y[7], z[7]) → EVAL(x[7], y[7], z[7]) which results in the following constraint:
  

  (39)    (z[10]=z[7]∧y[10]=y[7]∧x[10]=x[7]∧&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10]))=TRUE ⇒ COND_EVAL5(TRUE, x[7], y[7], z[7])≥NonInfC∧COND_EVAL5(TRUE, x[7], y[7], z[7])≥EVAL(x[7], y[7], z[7])∧(U^Increasing(EVAL(x[7], y[7], z[7])), ≥))

  
  
  We simplified constraint (39) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (40)    (>=@z(z[10], y[10])=TRUE∧>@z(x[10], z[10])=TRUE∧>=@z(z[10], x[10])=TRUE ⇒ COND_EVAL5(TRUE, x[10], y[10], z[10])≥NonInfC∧COND_EVAL5(TRUE, x[10], y[10], z[10])≥EVAL(x[10], y[10], z[10])∧(U^Increasing(EVAL(x[7], y[7], z[7])), ≥))

  
  
  We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (41)    (z[10] + (-1)y[10] ≥ 0∧-1 + x[10] + (-1)z[10] ≥ 0∧z[10] + (-1)x[10] ≥ 0 ⇒ (U^Increasing(EVAL(x[7], y[7], z[7])), ≥)∧0 ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (42)    (z[10] + (-1)y[10] ≥ 0∧-1 + x[10] + (-1)z[10] ≥ 0∧z[10] + (-1)x[10] ≥ 0 ⇒ (U^Increasing(EVAL(x[7], y[7], z[7])), ≥)∧0 ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (43)    (-1 + x[10] + (-1)z[10] ≥ 0∧z[10] + (-1)y[10] ≥ 0∧z[10] + (-1)x[10] ≥ 0 ⇒ (U^Increasing(EVAL(x[7], y[7], z[7])), ≥)∧-1 ≥ 0∧0 ≥ 0)

  
  
  We solved constraint (43) using rule (IDP_SMT_SPLIT).

• We consider the chain EVAL(x[10], y[10], z[10]) → COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10]) which results in the following constraint:
  

  (44)    (EVAL(x[10], y[10], z[10])≥NonInfC∧EVAL(x[10], y[10], z[10])≥COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥))

  
  
  We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (45)    ((U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (46)    ((U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (47)    (0 ≥ 0∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (48)    (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  

• We consider the chain EVAL(x[6], y[6], z[6]) → COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6]), COND_EVAL4(TRUE, x[4], y[4], z[4]) → EVAL(-@z(x[4], 1@z), y[4], z[4]) which results in the following constraint:
  

  (49)    (y[6]=y[4]∧x[6]=x[4]∧>@z(x[6], z[6])=TRUE∧z[6]=z[4] ⇒ COND_EVAL4(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL4(TRUE, x[4], y[4], z[4])≥EVAL(-@z(x[4], 1@z), y[4], z[4])∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (49) using rule (III) which results in the following new constraint:
  

  (50)    (>@z(x[6], z[6])=TRUE ⇒ COND_EVAL4(TRUE, x[6], y[6], z[6])≥NonInfC∧COND_EVAL4(TRUE, x[6], y[6], z[6])≥EVAL(-@z(x[6], 1@z), y[6], z[6])∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (51)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (52)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (53)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (54)    (x[6] + -1 + (-1)z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (54) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (55)    (x[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  We simplified constraint (55) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (56)    (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  

  (57)    (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))

  
  
  

• We consider the chain EVAL(x[6], y[6], z[6]) → COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6]) which results in the following constraint:
  

  (58)    (EVAL(x[6], y[6], z[6])≥NonInfC∧EVAL(x[6], y[6], z[6])≥COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥))

  
  
  We simplified constraint (58) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (59)    ((U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (59) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (60)    ((U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (60) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (61)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥))

  
  
  We simplified constraint (61) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (62)    (0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥))

  
  
  

• COND_EVAL1(TRUE, x[11], y[11], z[11]) → EVAL(x[11], -@z(y[11], 1@z), z[11])
  
  • (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧(-1)Bound + y[1] ≥ 0)
    
  • (x[1] ≥ 0∧y[1] ≥ 0∧z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(x[11], -@z(y[11], 1@z), z[11])), ≥)∧(-1)Bound + y[1] ≥ 0)
    
  
  
• EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])
  
  • (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(>@z(y[1], z[1]), >=@z(z[1], x[1])), x[1], y[1], z[1])), ≥)∧0 = 0∧0 = 0∧0 = 0)
    
  
  
• COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(-@z(x[0], 1@z), y[0], z[0])
  
  • (z[2] ≥ 0∧x[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))
    
  • (z[2] ≥ 0∧x[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(-@z(x[0], 1@z), y[0], z[0])), ≥))
    
  
  
• EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])
  
  • (0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL(&&(>@z(y[2], z[2]), >@z(x[2], z[2])), x[2], y[2], z[2])), ≥))
    
  
  
• COND_EVAL3(TRUE, x[8], y[8], z[8]) → EVAL(x[8], -@z(y[8], 1@z), z[8])
  
  
• EVAL(x[3], y[3], z[3]) → COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])
  
  • (0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL3(&&(&&(>@z(x[3], z[3]), >=@z(z[3], x[3])), >@z(y[3], z[3])), x[3], y[3], z[3])), ≥)∧0 ≥ 0)
    
  
  
• COND_EVAL5(TRUE, x[7], y[7], z[7]) → EVAL(x[7], y[7], z[7])
  
  
• EVAL(x[10], y[10], z[10]) → COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])
  
  • (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL5(&&(&&(>@z(x[10], z[10]), >=@z(z[10], x[10])), >=@z(z[10], y[10])), x[10], y[10], z[10])), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)
    
  
  
• COND_EVAL4(TRUE, x[4], y[4], z[4]) → EVAL(-@z(x[4], 1@z), y[4], z[4])
  
  • (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))
    
  • (x[6] ≥ 0∧z[6] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(-@z(x[4], 1@z), y[4], z[4])), ≥))
    
  
  
• EVAL(x[6], y[6], z[6]) → COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])
  
  • (0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL4(>@z(x[6], z[6]), x[6], y[6], z[6])), ≥))
    
  
  

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂   
POL(COND_EVAL3(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃   
POL(TRUE) = 0   
POL(&&(x₁, x₂)) = -1   
POL(EVAL(x₁, x₂, x₃)) = -1 + (-1)x₃ + x₂   
POL(FALSE) = 0   
POL(>@z(x₁, x₂)) = -1   
POL(COND_EVAL5(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃   
POL(>=@z(x₁, x₂)) = -1   
POL(COND_EVAL1(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃   
POL(COND_EVAL(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃   
POL(COND_EVAL4(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃   
POL(1@z) = 1   
POL(undefined) = -1